E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), e:E.
(rcv?(e))  sqequal(link(e); lnk(kind(e))) 

latex

Definitions	True, t  T, IdLnk, x:A  B(x), x.A(x), x:A. B(x), x. t(x), t.1, P  Q, False, b, lnk(k), rcv(l,tg), left + right, Id, f(a), x:AB(x), s = t, ecase1(e;info;i.f(i);l,e'.g(l;e')), kind(e), link(e), rcv?(e), Type, <a, b>, guard(T), sq_type(T), sqequal(s; t)
Lemmas	IdLnk sq, assert wf, rcv? wf, Id wf, false wf, pi1 wf, IdLnk wf, true wf